package joc.nextgen.dbi;

import static joc.nextgen.JOC.result;

import java.lang.ref.WeakReference;

import joc.nextgen.dbi.JOC.PostCondition;

class ObjectSpecContract implements ObjectSpec {
	private int hashCode;
	private boolean hashCodeSet = false;
	private WeakReference<Object> firstObject = null;

	@Override
	public boolean equals(final Object obj) {
		if (firstObject == null || firstObject.get() == null) {
			firstObject = new WeakReference<Object>(obj);
		}
		new PostCondition() {
			{
				if (obj == null) {
					assert result(boolean.class) == false : "if obj == null then false";
				} else {
					Object x = this;
					Object y = obj;
					Object z = firstObject.get();
					assert x.equals(x) : "is reflexive";
					assert x.equals(y) == y.equals(x) : "is symmetric";
					if (x.equals(y) && y.equals(z)) {
						assert x.equals(z) : "is transitive";
					}
					if (result(boolean.class)) {
						assert x.hashCode() == y.hashCode() : "is consistent with hashCode";
					}
				}
			}
		};
		return false;
	}

	@Override
	public int hashCode() {
		if (!hashCodeSet) {
			hashCode = hashCode();
			hashCodeSet = true;
		}
		new PostCondition() {
			{
				assert result(int.class) == hashCode : "is immutable";
			}
		};
		return 0;
	}

	@Override
	public String toString() {
		new PostCondition() {
			{
				assert result() != null : "not null";
			}
		};
		return null;
	}

}